\begin{tabbing}
FairFifo
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$i$:Id, $t$:$\mathbb{N}$, $l$:IdLnk. $\neg$source($l$) $=$ $i$ $\Rightarrow$ onlnk($l$;m($i$;$t$)) $=$ nil)\+
\\[0ex]\& ($\forall$$i$:Id, $t$:$\mathbb{N}$. isnull(a($i$;$t$)) $\Rightarrow$ ($\forall$$x$:Id. s($i$;$t$+1).$x$ $=$ s($i$;$t$).$x$) \& m($i$;$t$) $=$ nil)
\\[0ex]\& \=(\=$\forall$$i$:Id, $t$:$\mathbb{N}$, $l$:IdLnk.\+\+
\\[0ex]isrcv($l$;a($i$;$t$))
\\[0ex]$\Rightarrow$ destination($l$) $=$ $i$ \& $\parallel$queue($l$;$t$)$\parallel\geq$1 \& hd(queue($l$;$t$)) $=$ msg(a($i$;$t$)))
\-\\[0ex]\& \=($\forall$$l$:IdLnk, $t$:$\mathbb{N}$. $\exists$${\it t'}$:$\mathbb{N}$. $t$$\leq$${\it t'}$ \& isrcv($l$;a(destination($l$);${\it t'}$)) $\vee$ queue($l$;${\it t'}$) $=$ nil)\+
\\[0ex]\& w{-}machine{-}constraint($w$)
\\[0ex]\& w{-}atom{-}constraint($w$)
\-\-\-
\end{tabbing}